$\forall$$p$:(:$\mathbb{N}$ $\times$ $\mathbb{N}$). inc{-}fst($p$) $\in$ (:$\mathbb{N}$ $\times$ $\mathbb{N}$)